H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.927 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ CR

mainModule FiniteMap

((addListToFM_C :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a) :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap a b) where

addListToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> [(a,b)] -> FiniteMap a b

addListToFM_C

combiner fm key_elt_pairs

foldl add fm key_elt_pairs

where

add

fmap (key,elt)

addToFM_C combiner fmap key elt

addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b

addToFM_C

combiner EmptyFM key elt

unitFM key elt

addToFM_C

combiner (Branch key elt size fm_l fm_r) new_key new_elt

new_key < key

mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r

new_key > key

mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)

otherwise

Branch new_key (combiner elt new_elt) size fm_l fm_r

emptyFM :: FiniteMap a b

emptyFM

EmptyFM

findMax :: FiniteMap a b -> (a,b)

findMax	(Branch key elt _ _ EmptyFM)	=	(key,elt)
findMax	(Branch key elt _ _ fm_r)	=	findMax fm_r

findMin :: FiniteMap a b -> (a,b)

findMin	(Branch key elt _ EmptyFM _)	=	(key,elt)
findMin	(Branch key elt _ fm_l _)	=	findMin fm_l

mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBalBranch

key elt fm_L fm_R

size_l + size_r < 2

mkBranch 1 key elt fm_L fm_R

size_r > sIZE_RATIO * size_l

case

fm_R of

Branch _ _ _ fm_rl fm_rr

sizeFM fm_rl < 2 * sizeFM fm_rr

single_L fm_L fm_R

otherwise

double_L fm_L fm_R

size_l > sIZE_RATIO * size_r

case

fm_L of

Branch _ _ _ fm_ll fm_lr

sizeFM fm_lr < 2 * sizeFM fm_ll

single_R fm_L fm_R

otherwise

double_R fm_L fm_R

otherwise

mkBranch 2 key elt fm_L fm_R

where

double_L

fm_l (Branch key_r elt_r _ (Branch key_rl elt_rl _ fm_rll fm_rlr) fm_rr)

mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

double_R

(Branch key_l elt_l _ fm_ll (Branch key_lr elt_lr _ fm_lrl fm_lrr)) fm_r

mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)

single_L

fm_l (Branch key_r elt_r _ fm_rl fm_rr)

mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr

single_R

(Branch key_l elt_l _ fm_ll fm_lr) fm_r

mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)

size_l

sizeFM fm_L

size_r

sizeFM fm_R

mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBranch

which key elt fm_l fm_r

let

result

Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r

result

where

balance_ok

True

left_ok

case

fm_l of

EmptyFM

True

Branch left_key _ _ _ _

let

biggest_left_key

fst (findMax fm_l)

biggest_left_key < key

left_size

sizeFM fm_l

right_ok

case

fm_r of

EmptyFM

True

Branch right_key _ _ _ _

let

smallest_right_key

fst (findMin fm_r)

key < smallest_right_key

right_size

sizeFM fm_r

unbox :: Int -> Int

unbox

sIZE_RATIO :: Int

sIZE_RATIO

sizeFM :: FiniteMap a b -> Int

sizeFM	EmptyFM	=	0
sizeFM	(Branch _ _ size _ _)	=	size

unitFM :: a -> b -> FiniteMap a b

unitFM

key elt

Branch key elt 1 emptyFM emptyFM

module Maybe where

import qualified FiniteMap
import qualified Prelude

Case Reductions:
The following Case expression

case fm_l of
EmptyFM → True

Branch left_key _ _ _ _ →

let

biggest_left_key = fst (findMax fm_l)

in biggest_left_key < key

is transformed to

left_ok0 fm_l key EmptyFM = True

left_ok0 fm_l key (Branch left_key _ _ _ _) =

let

biggest_left_key = fst (findMax fm_l)

in biggest_left_key < key

The following Case expression

case fm_r of
EmptyFM → True

Branch right_key _ _ _ _ →

let

smallest_right_key = fst (findMin fm_r)

in key < smallest_right_key

is transformed to

right_ok0 fm_r key EmptyFM = True

right_ok0 fm_r key (Branch right_key _ _ _ _) =

let

smallest_right_key = fst (findMin fm_r)

in key < smallest_right_key

The following Case expression

case fm_R of
Branch _ _ _ fm_rl fm_rr

| sizeFM fm_rl < 2 * sizeFM fm_rr

→ single_L fm_L fm_R

| otherwise

→ double_L fm_L fm_R

is transformed to

mkBalBranch0 fm_L fm_R (Branch _ _ _ fm_rl fm_rr)

| sizeFM fm_rl < 2 * sizeFM fm_rr

= single_L fm_L fm_R

| otherwise

= double_L fm_L fm_R

The following Case expression

case fm_L of
Branch _ _ _ fm_ll fm_lr

| sizeFM fm_lr < 2 * sizeFM fm_ll

→ single_R fm_L fm_R

| otherwise

→ double_R fm_L fm_R

is transformed to

mkBalBranch1 fm_L fm_R (Branch _ _ _ fm_ll fm_lr)

| sizeFM fm_lr < 2 * sizeFM fm_ll

= single_R fm_L fm_R

| otherwise

= double_R fm_L fm_R

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule FiniteMap

((addListToFM_C :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a) :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap a b) where

addListToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> [(a,b)] -> FiniteMap a b

addListToFM_C

combiner fm key_elt_pairs

foldl add fm key_elt_pairs

where

add

fmap (key,elt)

addToFM_C combiner fmap key elt

addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a

addToFM_C

combiner EmptyFM key elt

unitFM key elt

addToFM_C

combiner (Branch key elt size fm_l fm_r) new_key new_elt

new_key < key

mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r

new_key > key

mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)

otherwise

Branch new_key (combiner elt new_elt) size fm_l fm_r

emptyFM :: FiniteMap a b

emptyFM

EmptyFM

findMax :: FiniteMap b a -> (b,a)

findMax	(Branch key elt _ _ EmptyFM)	=	(key,elt)
findMax	(Branch key elt _ _ fm_r)	=	findMax fm_r

findMin :: FiniteMap a b -> (a,b)

findMin	(Branch key elt _ EmptyFM _)	=	(key,elt)
findMin	(Branch key elt _ fm_l _)	=	findMin fm_l

mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a

mkBalBranch

key elt fm_L fm_R

size_l + size_r < 2

mkBranch 1 key elt fm_L fm_R

size_r > sIZE_RATIO * size_l

mkBalBranch0 fm_L fm_R fm_R

size_l > sIZE_RATIO * size_r

mkBalBranch1 fm_L fm_R fm_L

otherwise

mkBranch 2 key elt fm_L fm_R

where

double_L

fm_l (Branch key_r elt_r _ (Branch key_rl elt_rl _ fm_rll fm_rlr) fm_rr)

mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

double_R

(Branch key_l elt_l _ fm_ll (Branch key_lr elt_lr _ fm_lrl fm_lrr)) fm_r

mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)

mkBalBranch0

fm_L fm_R (Branch _ _ _ fm_rl fm_rr)

sizeFM fm_rl < 2 * sizeFM fm_rr

single_L fm_L fm_R

otherwise

double_L fm_L fm_R

mkBalBranch1

fm_L fm_R (Branch _ _ _ fm_ll fm_lr)

sizeFM fm_lr < 2 * sizeFM fm_ll

single_R fm_L fm_R

otherwise

double_R fm_L fm_R

single_L

fm_l (Branch key_r elt_r _ fm_rl fm_rr)

mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr

single_R

(Branch key_l elt_l _ fm_ll fm_lr) fm_r

mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)

size_l

sizeFM fm_L

size_r

sizeFM fm_R

mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBranch

which key elt fm_l fm_r

let

result

Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r

result

where

balance_ok

True

left_ok

left_ok0 fm_l key fm_l

left_ok0

fm_l key EmptyFM

True

left_ok0

fm_l key (Branch left_key _ _ _ _)

let

biggest_left_key

fst (findMax fm_l)

biggest_left_key < key

left_size

sizeFM fm_l

right_ok

right_ok0 fm_r key fm_r

right_ok0

fm_r key EmptyFM

True

right_ok0

fm_r key (Branch right_key _ _ _ _)

let

smallest_right_key

fst (findMin fm_r)

key < smallest_right_key

right_size

sizeFM fm_r

unbox :: Int -> Int

unbox

sIZE_RATIO :: Int

sIZE_RATIO

sizeFM :: FiniteMap b a -> Int

sizeFM	EmptyFM	=	0
sizeFM	(Branch _ _ size _ _)	=	size

unitFM :: a -> b -> FiniteMap a b

unitFM

key elt

Branch key elt 1 emptyFM emptyFM

module Maybe where

import qualified FiniteMap
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule FiniteMap

((addListToFM_C :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a) :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap a b) where

addListToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> [(a,b)] -> FiniteMap a b

addListToFM_C

combiner fm key_elt_pairs

foldl add fm key_elt_pairs

where

add

fmap (key,elt)

addToFM_C combiner fmap key elt

addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b

addToFM_C

combiner EmptyFM key elt

unitFM key elt

addToFM_C

combiner (Branch key elt size fm_l fm_r) new_key new_elt

new_key < key

mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r

new_key > key

mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)

otherwise

Branch new_key (combiner elt new_elt) size fm_l fm_r

emptyFM :: FiniteMap a b

emptyFM

EmptyFM

findMax :: FiniteMap a b -> (a,b)

findMax	(Branch key elt xw xx EmptyFM)	=	(key,elt)
findMax	(Branch key elt xy xz fm_r)	=	findMax fm_r

findMin :: FiniteMap b a -> (b,a)

findMin	(Branch key elt wy EmptyFM wz)	=	(key,elt)
findMin	(Branch key elt xu fm_l xv)	=	findMin fm_l

mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBalBranch

key elt fm_L fm_R

size_l + size_r < 2

mkBranch 1 key elt fm_L fm_R

size_r > sIZE_RATIO * size_l

mkBalBranch0 fm_L fm_R fm_R

size_l > sIZE_RATIO * size_r

mkBalBranch1 fm_L fm_R fm_L

otherwise

mkBranch 2 key elt fm_L fm_R

where

double_L

fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr)

mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

double_R

(Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r

mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)

mkBalBranch0

fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

sizeFM fm_rl < 2 * sizeFM fm_rr

single_L fm_L fm_R

otherwise

double_L fm_L fm_R

mkBalBranch1

fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

sizeFM fm_lr < 2 * sizeFM fm_ll

single_R fm_L fm_R

otherwise

double_R fm_L fm_R

single_L

fm_l (Branch key_r elt_r vux fm_rl fm_rr)

mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr

single_R

(Branch key_l elt_l yy fm_ll fm_lr) fm_r

mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)

size_l

sizeFM fm_L

size_r

sizeFM fm_R

mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBranch

which key elt fm_l fm_r

let

result

Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r

result

where

balance_ok

True

left_ok

left_ok0 fm_l key fm_l

left_ok0

fm_l key EmptyFM

True

left_ok0

fm_l key (Branch left_key wu wv ww wx)

let

biggest_left_key

fst (findMax fm_l)

biggest_left_key < key

left_size

sizeFM fm_l

right_ok

right_ok0 fm_r key fm_r

right_ok0

fm_r key EmptyFM

True

right_ok0

fm_r key (Branch right_key vw vx vy vz)

let

smallest_right_key

fst (findMin fm_r)

key < smallest_right_key

right_size

sizeFM fm_r

unbox :: Int -> Int

unbox

sIZE_RATIO :: Int

sIZE_RATIO

sizeFM :: FiniteMap a b -> Int

sizeFM	EmptyFM	=	0
sizeFM	(Branch yu yv size yw yx)	=	size

unitFM :: a -> b -> FiniteMap a b

unitFM

key elt

Branch key elt 1 emptyFM emptyFM

module Maybe where

import qualified FiniteMap
import qualified Prelude

Cond Reductions:
The following Function with conditions

addToFM_C combiner EmptyFM key elt = unitFM key elt

addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt

| new_key < key

= mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r

| new_key > key

= mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)

| otherwise

= Branch new_key (combiner elt new_elt) size fm_l fm_r

is transformed to

addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt

addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r

addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)

addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

addToFM_C4 combiner EmptyFM key elt = unitFM key elt

addToFM_C4 vvx vvy vvz vwu = addToFM_C3 vvx vvy vvz vwu

The following Function with conditions

mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

| sizeFM fm_lr < 2 * sizeFM fm_ll

= single_R fm_L fm_R

| otherwise

= double_R fm_L fm_R

is transformed to

mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr True = single_R fm_L fm_R

mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr True = double_R fm_L fm_R

mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

The following Function with conditions

mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

| sizeFM fm_rl < 2 * sizeFM fm_rr

= single_L fm_L fm_R

| otherwise

= double_L fm_L fm_R

is transformed to

mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = single_L fm_L fm_R

mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = double_L fm_L fm_R

mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

The following Function with conditions

mkBalBranch key elt fm_L fm_R

| size_l + size_r < 2

= mkBranch 1 key elt fm_L fm_R

| size_r > sIZE_RATIO * size_l

= mkBalBranch0 fm_L fm_R fm_R

| size_l > sIZE_RATIO * size_r

= mkBalBranch1 fm_L fm_R fm_L

| otherwise

= mkBranch 2 key elt fm_L fm_R

where

double_L fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

double_R (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)

mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

| sizeFM fm_rl < 2 * sizeFM fm_rr

= single_L fm_L fm_R

| otherwise

= double_L fm_L fm_R

mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

| sizeFM fm_lr < 2 * sizeFM fm_ll

= single_R fm_L fm_R

| otherwise

= double_R fm_L fm_R

single_L fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr

single_R (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)

size_l = sizeFM fm_L

size_r = sizeFM fm_R

is transformed to

mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

mkBalBranch6 key elt fm_L fm_R =

mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2)

where

double_L fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

double_R (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)

mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = double_L fm_L fm_R

mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = single_L fm_L fm_R

mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr True = double_R fm_L fm_R

mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr True = single_R fm_L fm_R

mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R

mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L

mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise

mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R

mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)

mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R

mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)

single_L fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr

single_R (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)

size_l = sizeFM fm_L

size_r = sizeFM fm_R

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule FiniteMap

((addListToFM_C :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a) :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

addListToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> [(a,b)] -> FiniteMap a b

addListToFM_C

combiner fm key_elt_pairs

foldl add fm key_elt_pairs

where

add

fmap (key,elt)

addToFM_C combiner fmap key elt

addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a

addToFM_C	combiner EmptyFM key elt	=	addToFM_C4 combiner EmptyFM key elt
addToFM_C	combiner (Branch key elt size fm_l fm_r) new_key new_elt	=	addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C0

combiner key elt size fm_l fm_r new_key new_elt True

Branch new_key (combiner elt new_elt) size fm_l fm_r

addToFM_C1	combiner key elt size fm_l fm_r new_key new_elt True	=	mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1	combiner key elt size fm_l fm_r new_key new_elt False	=	addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

addToFM_C2	combiner key elt size fm_l fm_r new_key new_elt True	=	mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2	combiner key elt size fm_l fm_r new_key new_elt False	=	addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

addToFM_C3

combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

addToFM_C4	combiner EmptyFM key elt	=	unitFM key elt
addToFM_C4	vvx vvy vvz vwu	=	addToFM_C3 vvx vvy vvz vwu

emptyFM :: FiniteMap a b

emptyFM

EmptyFM

findMax :: FiniteMap b a -> (b,a)

findMax	(Branch key elt xw xx EmptyFM)	=	(key,elt)
findMax	(Branch key elt xy xz fm_r)	=	findMax fm_r

findMin :: FiniteMap b a -> (b,a)

findMin	(Branch key elt wy EmptyFM wz)	=	(key,elt)
findMin	(Branch key elt xu fm_l xv)	=	findMin fm_l

mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBalBranch

key elt fm_L fm_R

mkBalBranch6 key elt fm_L fm_R

mkBalBranch6

key elt fm_L fm_R

mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2)

where

double_L

fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr)

mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

double_R

(Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r

mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)

mkBalBranch0

fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch00

fm_L fm_R vuu vuv vuw fm_rl fm_rr True

double_L fm_L fm_R

mkBalBranch01	fm_L fm_R vuu vuv vuw fm_rl fm_rr True	=	single_L fm_L fm_R
mkBalBranch01	fm_L fm_R vuu vuv vuw fm_rl fm_rr False	=	mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBalBranch02

fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

mkBalBranch1

fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch10

fm_L fm_R yz zu zv fm_ll fm_lr True

double_R fm_L fm_R

mkBalBranch11	fm_L fm_R yz zu zv fm_ll fm_lr True	=	single_R fm_L fm_R
mkBalBranch11	fm_L fm_R yz zu zv fm_ll fm_lr False	=	mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch12

fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

mkBalBranch2

key elt fm_L fm_R True

mkBranch 2 key elt fm_L fm_R

mkBalBranch3	key elt fm_L fm_R True	=	mkBalBranch1 fm_L fm_R fm_L
mkBalBranch3	key elt fm_L fm_R False	=	mkBalBranch2 key elt fm_L fm_R otherwise

mkBalBranch4	key elt fm_L fm_R True	=	mkBalBranch0 fm_L fm_R fm_R
mkBalBranch4	key elt fm_L fm_R False	=	mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)

mkBalBranch5	key elt fm_L fm_R True	=	mkBranch 1 key elt fm_L fm_R
mkBalBranch5	key elt fm_L fm_R False	=	mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)

single_L

fm_l (Branch key_r elt_r vux fm_rl fm_rr)

mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr

single_R

(Branch key_l elt_l yy fm_ll fm_lr) fm_r

mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)

size_l

sizeFM fm_L

size_r

sizeFM fm_R

mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBranch

which key elt fm_l fm_r

let

result

Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r

result

where

balance_ok

True

left_ok

left_ok0 fm_l key fm_l

left_ok0

fm_l key EmptyFM

True

left_ok0

fm_l key (Branch left_key wu wv ww wx)

let

biggest_left_key

fst (findMax fm_l)

biggest_left_key < key

left_size

sizeFM fm_l

right_ok

right_ok0 fm_r key fm_r

right_ok0

fm_r key EmptyFM

True

right_ok0

fm_r key (Branch right_key vw vx vy vz)

let

smallest_right_key

fst (findMin fm_r)

key < smallest_right_key

right_size

sizeFM fm_r

unbox :: Int -> Int

unbox

sIZE_RATIO :: Int

sIZE_RATIO

sizeFM :: FiniteMap b a -> Int

sizeFM	EmptyFM	=	0
sizeFM	(Branch yu yv size yw yx)	=	size

unitFM :: b -> a -> FiniteMap b a

unitFM

key elt

Branch key elt 1 emptyFM emptyFM

module Maybe where

import qualified FiniteMap
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

let

result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r

in result

where

balance_ok = True

left_ok = left_ok0 fm_l key fm_l

left_ok0 fm_l key EmptyFM = True

left_ok0 fm_l key (Branch left_key wu wv ww wx) =

let

biggest_left_key = fst (findMax fm_l)

in biggest_left_key < key

left_size = sizeFM fm_l

right_ok = right_ok0 fm_r key fm_r

right_ok0 fm_r key EmptyFM = True

right_ok0 fm_r key (Branch right_key vw vx vy vz) =

let

smallest_right_key = fst (findMin fm_r)

in key < smallest_right_key

right_size = sizeFM fm_r

unbox x = x

are unpacked to the following functions on top level

mkBranchLeft_ok0 vwx vwy vwz fm_l key EmptyFM = True

mkBranchLeft_ok0 vwx vwy vwz fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key

mkBranchLeft_size vwx vwy vwz = sizeFM vwx

mkBranchRight_ok vwx vwy vwz = mkBranchRight_ok0 vwx vwy vwz vwy vwz vwy

mkBranchLeft_ok vwx vwy vwz = mkBranchLeft_ok0 vwx vwy vwz vwx vwz vwx

mkBranchRight_size vwx vwy vwz = sizeFM vwy

mkBranchUnbox vwx vwy vwz x = x

mkBranchBalance_ok vwx vwy vwz = True

mkBranchRight_ok0 vwx vwy vwz fm_r key EmptyFM = True

mkBranchRight_ok0 vwx vwy vwz fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r

The bindings of the following Let/Where expression

let

result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r

in result

are unpacked to the following functions on top level

mkBranchResult vxu vxv vxw vxx = Branch vxu vxv (mkBranchUnbox vxw vxx vxu (1 + mkBranchLeft_size vxw vxx vxu + mkBranchRight_size vxw vxx vxu)) vxw vxx

The bindings of the following Let/Where expression

mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2)

where

double_L fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

double_R (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)

mkBalBranch0 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = double_L fm_L fm_R

mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr True = single_L fm_L fm_R

mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBalBranch02 fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

mkBalBranch1 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr True = double_R fm_L fm_R

mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr True = single_R fm_L fm_R

mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch12 fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch11 fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R

mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L

mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise

mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R

mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)

mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R

mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)

single_L fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr

single_R (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)

size_l = sizeFM fm_L

size_r = sizeFM fm_R

are unpacked to the following functions on top level

mkBalBranch6Double_R vxy vxz vyu vyv (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 vxy vxz fm_lrr fm_r)

mkBalBranch6MkBalBranch5 vxy vxz vyu vyv key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R

mkBalBranch6MkBalBranch5 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_r vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_l vxy vxz vyu vyv)

mkBalBranch6Size_l vxy vxz vyu vyv = sizeFM vyu

mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

mkBalBranch6Single_R vxy vxz vyu vyv (Branch key_l elt_l yy fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 vxy vxz fm_lr fm_r)

mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R

mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr) = mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch6Double_L vxy vxz vyu vyv fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 vxy vxz fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R fm_R

mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_l vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_r vxy vxz vyu vyv)

mkBalBranch6Size_r vxy vxz vyu vyv = sizeFM vyv

mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True = mkBalBranch6Single_R vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr False = mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R fm_L

mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R otherwise

mkBalBranch6Single_L vxy vxz vyu vyv fm_l (Branch key_r elt_r vux fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 vxy vxz fm_l fm_rl) fm_rr

mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True = mkBalBranch6Double_R vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True = mkBalBranch6Double_L vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr) = mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True = mkBalBranch6Single_L vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr False = mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

The bindings of the following Let/Where expression

foldl add fm key_elt_pairs

where

add fmap (key,elt) = addToFM_C combiner fmap key elt

are unpacked to the following functions on top level

addListToFM_CAdd vyw fmap (key,elt) = addToFM_C vyw fmap key elt

The bindings of the following Let/Where expression

let

biggest_left_key = fst (findMax fm_l)

in biggest_left_key < key

are unpacked to the following functions on top level

mkBranchLeft_ok0Biggest_left_key vyx = fst (findMax vyx)

The bindings of the following Let/Where expression

let

smallest_right_key = fst (findMin fm_r)

in key < smallest_right_key

are unpacked to the following functions on top level

mkBranchRight_ok0Smallest_right_key vyy = fst (findMin vyy)

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

mainModule FiniteMap

((addListToFM_C :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a) :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

addListToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> [(b,a)] -> FiniteMap b a

addListToFM_C

combiner fm key_elt_pairs

foldl (addListToFM_CAdd combiner) fm key_elt_pairs

addListToFM_CAdd

vyw fmap (key,elt)

addToFM_C vyw fmap key elt

addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b

addToFM_C	combiner EmptyFM key elt	=	addToFM_C4 combiner EmptyFM key elt
addToFM_C	combiner (Branch key elt size fm_l fm_r) new_key new_elt	=	addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C0

combiner key elt size fm_l fm_r new_key new_elt True

Branch new_key (combiner elt new_elt) size fm_l fm_r

addToFM_C1	combiner key elt size fm_l fm_r new_key new_elt True	=	mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1	combiner key elt size fm_l fm_r new_key new_elt False	=	addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

addToFM_C2	combiner key elt size fm_l fm_r new_key new_elt True	=	mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2	combiner key elt size fm_l fm_r new_key new_elt False	=	addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

addToFM_C3

combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

addToFM_C4	combiner EmptyFM key elt	=	unitFM key elt
addToFM_C4	vvx vvy vvz vwu	=	addToFM_C3 vvx vvy vvz vwu

emptyFM :: FiniteMap b a

emptyFM

EmptyFM

findMax :: FiniteMap b a -> (b,a)

findMax	(Branch key elt xw xx EmptyFM)	=	(key,elt)
findMax	(Branch key elt xy xz fm_r)	=	findMax fm_r

findMin :: FiniteMap b a -> (b,a)

findMin	(Branch key elt wy EmptyFM wz)	=	(key,elt)
findMin	(Branch key elt xu fm_l xv)	=	findMin fm_l

mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBalBranch

key elt fm_L fm_R

mkBalBranch6 key elt fm_L fm_R

mkBalBranch6

key elt fm_L fm_R

mkBalBranch6MkBalBranch5 key elt fm_L fm_R key elt fm_L fm_R (mkBalBranch6Size_l key elt fm_L fm_R + mkBalBranch6Size_r key elt fm_L fm_R < 2)

mkBalBranch6Double_L

vxy vxz vyu vyv fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr)

mkBranch 5 key_rl elt_rl (mkBranch 6 vxy vxz fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

mkBalBranch6Double_R

vxy vxz vyu vyv (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r

mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 vxy vxz fm_lrr fm_r)

mkBalBranch6MkBalBranch0

vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch6MkBalBranch00

vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True

mkBalBranch6Double_L vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch01	vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True	=	mkBalBranch6Single_L vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch01	vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr False	=	mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBalBranch6MkBalBranch02

vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

mkBalBranch6MkBalBranch1

vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch6MkBalBranch10

vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True

mkBalBranch6Double_R vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch11	vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True	=	mkBalBranch6Single_R vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch11	vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr False	=	mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch6MkBalBranch12

vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

mkBalBranch6MkBalBranch2

vxy vxz vyu vyv key elt fm_L fm_R True

mkBranch 2 key elt fm_L fm_R

mkBalBranch6MkBalBranch3	vxy vxz vyu vyv key elt fm_L fm_R True	=	mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R fm_L
mkBalBranch6MkBalBranch3	vxy vxz vyu vyv key elt fm_L fm_R False	=	mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R otherwise

mkBalBranch6MkBalBranch4	vxy vxz vyu vyv key elt fm_L fm_R True	=	mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R fm_R
mkBalBranch6MkBalBranch4	vxy vxz vyu vyv key elt fm_L fm_R False	=	mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_l vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_r vxy vxz vyu vyv)

mkBalBranch6MkBalBranch5	vxy vxz vyu vyv key elt fm_L fm_R True	=	mkBranch 1 key elt fm_L fm_R
mkBalBranch6MkBalBranch5	vxy vxz vyu vyv key elt fm_L fm_R False	=	mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_r vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_l vxy vxz vyu vyv)

mkBalBranch6Single_L

vxy vxz vyu vyv fm_l (Branch key_r elt_r vux fm_rl fm_rr)

mkBranch 3 key_r elt_r (mkBranch 4 vxy vxz fm_l fm_rl) fm_rr

mkBalBranch6Single_R

vxy vxz vyu vyv (Branch key_l elt_l yy fm_ll fm_lr) fm_r

mkBranch 8 key_l elt_l fm_ll (mkBranch 9 vxy vxz fm_lr fm_r)

mkBalBranch6Size_l

vxy vxz vyu vyv

sizeFM vyu

mkBalBranch6Size_r

vxy vxz vyu vyv

sizeFM vyv

mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a

mkBranch

which key elt fm_l fm_r

mkBranchResult key elt fm_l fm_r

mkBranchBalance_ok

vwx vwy vwz

True

mkBranchLeft_ok

vwx vwy vwz

mkBranchLeft_ok0 vwx vwy vwz vwx vwz vwx

mkBranchLeft_ok0	vwx vwy vwz fm_l key EmptyFM	=	True
mkBranchLeft_ok0	vwx vwy vwz fm_l key (Branch left_key wu wv ww wx)	=	mkBranchLeft_ok0Biggest_left_key fm_l < key

mkBranchLeft_ok0Biggest_left_key

vyx

fst (findMax vyx)

mkBranchLeft_size

vwx vwy vwz

sizeFM vwx

mkBranchResult

vxu vxv vxw vxx

Branch vxu vxv (mkBranchUnbox vxw vxx vxu (1 + mkBranchLeft_size vxw vxx vxu + mkBranchRight_size vxw vxx vxu)) vxw vxx

mkBranchRight_ok

vwx vwy vwz

mkBranchRight_ok0 vwx vwy vwz vwy vwz vwy

mkBranchRight_ok0	vwx vwy vwz fm_r key EmptyFM	=	True
mkBranchRight_ok0	vwx vwy vwz fm_r key (Branch right_key vw vx vy vz)	=	key < mkBranchRight_ok0Smallest_right_key fm_r

mkBranchRight_ok0Smallest_right_key

vyy

fst (findMin vyy)

mkBranchRight_size

vwx vwy vwz

sizeFM vwy

mkBranchUnbox :: Ord a => -> (FiniteMap a b) ( -> (FiniteMap a b) ( -> a (Int -> Int)))

mkBranchUnbox

vwx vwy vwz x

sIZE_RATIO :: Int

sIZE_RATIO

sizeFM :: FiniteMap a b -> Int

sizeFM	EmptyFM	=	0
sizeFM	(Branch yu yv size yw yx)	=	size

unitFM :: b -> a -> FiniteMap b a

unitFM

key elt

Branch key elt 1 emptyFM emptyFM

module Maybe where

import qualified FiniteMap
import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

mainModule FiniteMap

(addListToFM_C :: (a -> a -> a) -> FiniteMap () a -> [((),a)] -> FiniteMap () a)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap a b) where

addListToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> [(a,b)] -> FiniteMap a b

addListToFM_C

combiner fm key_elt_pairs

foldl (addListToFM_CAdd combiner) fm key_elt_pairs

addListToFM_CAdd

vyw fmap (key,elt)

addToFM_C vyw fmap key elt

addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b

addToFM_C	combiner EmptyFM key elt	=	addToFM_C4 combiner EmptyFM key elt
addToFM_C	combiner (Branch key elt size fm_l fm_r) new_key new_elt	=	addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C0

combiner key elt size fm_l fm_r new_key new_elt True

Branch new_key (combiner elt new_elt) size fm_l fm_r

addToFM_C1	combiner key elt size fm_l fm_r new_key new_elt True	=	mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1	combiner key elt size fm_l fm_r new_key new_elt False	=	addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

addToFM_C2	combiner key elt size fm_l fm_r new_key new_elt True	=	mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2	combiner key elt size fm_l fm_r new_key new_elt False	=	addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

addToFM_C3

combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

addToFM_C4	combiner EmptyFM key elt	=	unitFM key elt
addToFM_C4	vvx vvy vvz vwu	=	addToFM_C3 vvx vvy vvz vwu

emptyFM :: FiniteMap a b

emptyFM

EmptyFM

findMax :: FiniteMap a b -> (a,b)

findMax	(Branch key elt xw xx EmptyFM)	=	(key,elt)
findMax	(Branch key elt xy xz fm_r)	=	findMax fm_r

findMin :: FiniteMap b a -> (b,a)

findMin	(Branch key elt wy EmptyFM wz)	=	(key,elt)
findMin	(Branch key elt xu fm_l xv)	=	findMin fm_l

mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a

mkBalBranch

key elt fm_L fm_R

mkBalBranch6 key elt fm_L fm_R

mkBalBranch6

key elt fm_L fm_R

mkBalBranch6MkBalBranch5 key elt fm_L fm_R key elt fm_L fm_R (mkBalBranch6Size_l key elt fm_L fm_R + mkBalBranch6Size_r key elt fm_L fm_R < Pos (Succ (Succ Zero)))

mkBalBranch6Double_L

vxy vxz vyu vyv fm_l (Branch key_r elt_r zy (Branch key_rl elt_rl zz fm_rll fm_rlr) fm_rr)

mkBranch (Pos (Succ (Succ (Succ (Succ (Succ Zero)))))) key_rl elt_rl (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))) vxy vxz fm_l fm_rll) (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))) key_r elt_r fm_rlr fm_rr)

mkBalBranch6Double_R

vxy vxz vyu vyv (Branch key_l elt_l zw fm_ll (Branch key_lr elt_lr zx fm_lrl fm_lrr)) fm_r

mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))) key_lr elt_lr (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))) key_l elt_l fm_ll fm_lrl) (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))) vxy vxz fm_lrr fm_r)

mkBalBranch6MkBalBranch0

vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch6MkBalBranch02 vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch6MkBalBranch00

vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True

mkBalBranch6Double_L vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch01	vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True	=	mkBalBranch6Single_L vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch01	vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr False	=	mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBalBranch6MkBalBranch02

vxy vxz vyu vyv fm_L fm_R (Branch vuu vuv vuw fm_rl fm_rr)

mkBalBranch6MkBalBranch01 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr (sizeFM fm_rl < Pos (Succ (Succ Zero)) * sizeFM fm_rr)

mkBalBranch6MkBalBranch1

vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch6MkBalBranch12 vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch6MkBalBranch10

vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True

mkBalBranch6Double_R vxy vxz vyu vyv fm_L fm_R

mkBalBranch6MkBalBranch11	vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True	=	mkBalBranch6Single_R vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch11	vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr False	=	mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch6MkBalBranch12

vxy vxz vyu vyv fm_L fm_R (Branch yz zu zv fm_ll fm_lr)

mkBalBranch6MkBalBranch11 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr (sizeFM fm_lr < Pos (Succ (Succ Zero)) * sizeFM fm_ll)

mkBalBranch6MkBalBranch2

vxy vxz vyu vyv key elt fm_L fm_R True

mkBranch (Pos (Succ (Succ Zero))) key elt fm_L fm_R

mkBalBranch6MkBalBranch3	vxy vxz vyu vyv key elt fm_L fm_R True	=	mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R fm_L
mkBalBranch6MkBalBranch3	vxy vxz vyu vyv key elt fm_L fm_R False	=	mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R otherwise

mkBalBranch6MkBalBranch4	vxy vxz vyu vyv key elt fm_L fm_R True	=	mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R fm_R
mkBalBranch6MkBalBranch4	vxy vxz vyu vyv key elt fm_L fm_R False	=	mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_l vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_r vxy vxz vyu vyv)

mkBalBranch6MkBalBranch5	vxy vxz vyu vyv key elt fm_L fm_R True	=	mkBranch (Pos (Succ Zero)) key elt fm_L fm_R
mkBalBranch6MkBalBranch5	vxy vxz vyu vyv key elt fm_L fm_R False	=	mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_r vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_l vxy vxz vyu vyv)

mkBalBranch6Single_L

vxy vxz vyu vyv fm_l (Branch key_r elt_r vux fm_rl fm_rr)

mkBranch (Pos (Succ (Succ (Succ Zero)))) key_r elt_r (mkBranch (Pos (Succ (Succ (Succ (Succ Zero))))) vxy vxz fm_l fm_rl) fm_rr

mkBalBranch6Single_R

vxy vxz vyu vyv (Branch key_l elt_l yy fm_ll fm_lr) fm_r

mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))) key_l elt_l fm_ll (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))) vxy vxz fm_lr fm_r)

mkBalBranch6Size_l

vxy vxz vyu vyv

sizeFM vyu

mkBalBranch6Size_r

vxy vxz vyu vyv

sizeFM vyv

mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b

mkBranch

which key elt fm_l fm_r

mkBranchResult key elt fm_l fm_r

mkBranchBalance_ok

vwx vwy vwz

True

mkBranchLeft_ok

vwx vwy vwz

mkBranchLeft_ok0 vwx vwy vwz vwx vwz vwx

mkBranchLeft_ok0	vwx vwy vwz fm_l key EmptyFM	=	True
mkBranchLeft_ok0	vwx vwy vwz fm_l key (Branch left_key wu wv ww wx)	=	mkBranchLeft_ok0Biggest_left_key fm_l < key

mkBranchLeft_ok0Biggest_left_key

vyx

fst (findMax vyx)

mkBranchLeft_size

vwx vwy vwz

sizeFM vwx

mkBranchResult

vxu vxv vxw vxx

Branch vxu vxv (mkBranchUnbox vxw vxx vxu (Pos (Succ Zero) + mkBranchLeft_size vxw vxx vxu + mkBranchRight_size vxw vxx vxu)) vxw vxx

mkBranchRight_ok

vwx vwy vwz

mkBranchRight_ok0 vwx vwy vwz vwy vwz vwy

mkBranchRight_ok0	vwx vwy vwz fm_r key EmptyFM	=	True
mkBranchRight_ok0	vwx vwy vwz fm_r key (Branch right_key vw vx vy vz)	=	key < mkBranchRight_ok0Smallest_right_key fm_r

mkBranchRight_ok0Smallest_right_key

vyy

fst (findMin vyy)

mkBranchRight_size

vwx vwy vwz

sizeFM vwy

mkBranchUnbox :: Ord a => -> (FiniteMap a b) ( -> (FiniteMap a b) ( -> a (Int -> Int)))

mkBranchUnbox

vwx vwy vwz x

sIZE_RATIO :: Int

sIZE_RATIO

Pos (Succ (Succ (Succ (Succ (Succ Zero)))))

sizeFM :: FiniteMap b a -> Int

sizeFM	EmptyFM	=	Pos Zero
sizeFM	(Branch yu yv size yw yx)	=	size

unitFM :: b -> a -> FiniteMap b a

unitFM

key elt

Branch key elt (Pos (Succ Zero)) emptyFM emptyFM

module Maybe where

import qualified FiniteMap
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="addListToFM_C",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="addListToFM_C vyz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="addListToFM_C vyz3 vyz4",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="addListToFM_C vyz3 vyz4 vyz5",fontsize=16,color="black",shape="triangle"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="foldl (addListToFM_CAdd vyz3) vyz4 vyz5",fontsize=16,color="burlywood",shape="triangle"];40[label="vyz5/vyz50 : vyz51",fontsize=10,color="white",style="solid",shape="box"];6 -> 40[label="",style="solid", color="burlywood", weight=9];
40 -> 7[label="",style="solid", color="burlywood", weight=3];
41[label="vyz5/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 41[label="",style="solid", color="burlywood", weight=9];
41 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="foldl (addListToFM_CAdd vyz3) vyz4 (vyz50 : vyz51)",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="foldl (addListToFM_CAdd vyz3) vyz4 []",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9 -> 6[label="",style="dashed", color="red", weight=0];
9[label="foldl (addListToFM_CAdd vyz3) (addListToFM_CAdd vyz3 vyz4 vyz50) vyz51",fontsize=16,color="magenta"];9 -> 11[label="",style="dashed", color="magenta", weight=3];
9 -> 12[label="",style="dashed", color="magenta", weight=3];
10[label="vyz4",fontsize=16,color="green",shape="box"];11[label="vyz51",fontsize=16,color="green",shape="box"];12[label="addListToFM_CAdd vyz3 vyz4 vyz50",fontsize=16,color="burlywood",shape="box"];43[label="vyz50/(vyz500,vyz501)",fontsize=10,color="white",style="solid",shape="box"];12 -> 43[label="",style="solid", color="burlywood", weight=9];
43 -> 13[label="",style="solid", color="burlywood", weight=3];
13[label="addListToFM_CAdd vyz3 vyz4 (vyz500,vyz501)",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="addToFM_C vyz3 vyz4 vyz500 vyz501",fontsize=16,color="burlywood",shape="box"];44[label="vyz4/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];14 -> 44[label="",style="solid", color="burlywood", weight=9];
44 -> 15[label="",style="solid", color="burlywood", weight=3];
45[label="vyz4/Branch vyz40 vyz41 vyz42 vyz43 vyz44",fontsize=10,color="white",style="solid",shape="box"];14 -> 45[label="",style="solid", color="burlywood", weight=9];
45 -> 16[label="",style="solid", color="burlywood", weight=3];
15[label="addToFM_C vyz3 EmptyFM vyz500 vyz501",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="addToFM_C vyz3 (Branch vyz40 vyz41 vyz42 vyz43 vyz44) vyz500 vyz501",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="addToFM_C4 vyz3 EmptyFM vyz500 vyz501",fontsize=16,color="black",shape="box"];17 -> 19[label="",style="solid", color="black", weight=3];
18[label="addToFM_C3 vyz3 (Branch vyz40 vyz41 vyz42 vyz43 vyz44) vyz500 vyz501",fontsize=16,color="black",shape="box"];18 -> 20[label="",style="solid", color="black", weight=3];
19[label="unitFM vyz500 vyz501",fontsize=16,color="black",shape="box"];19 -> 21[label="",style="solid", color="black", weight=3];
20[label="addToFM_C2 vyz3 vyz40 vyz41 vyz42 vyz43 vyz44 vyz500 vyz501 (vyz500 < vyz40)",fontsize=16,color="black",shape="box"];20 -> 22[label="",style="solid", color="black", weight=3];
21[label="Branch vyz500 vyz501 (Pos (Succ Zero)) emptyFM emptyFM",fontsize=16,color="green",shape="box"];21 -> 23[label="",style="dashed", color="green", weight=3];
21 -> 24[label="",style="dashed", color="green", weight=3];
22[label="addToFM_C2 vyz3 vyz40 vyz41 vyz42 vyz43 vyz44 vyz500 vyz501 (compare vyz500 vyz40 == LT)",fontsize=16,color="burlywood",shape="box"];46[label="vyz500/()",fontsize=10,color="white",style="solid",shape="box"];22 -> 46[label="",style="solid", color="burlywood", weight=9];
46 -> 25[label="",style="solid", color="burlywood", weight=3];
23[label="emptyFM",fontsize=16,color="black",shape="triangle"];23 -> 26[label="",style="solid", color="black", weight=3];
24 -> 23[label="",style="dashed", color="red", weight=0];
24[label="emptyFM",fontsize=16,color="magenta"];25[label="addToFM_C2 vyz3 vyz40 vyz41 vyz42 vyz43 vyz44 () vyz501 (compare () vyz40 == LT)",fontsize=16,color="burlywood",shape="box"];48[label="vyz40/()",fontsize=10,color="white",style="solid",shape="box"];25 -> 48[label="",style="solid", color="burlywood", weight=9];
48 -> 27[label="",style="solid", color="burlywood", weight=3];
26[label="EmptyFM",fontsize=16,color="green",shape="box"];27[label="addToFM_C2 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 (compare () () == LT)",fontsize=16,color="black",shape="box"];27 -> 28[label="",style="solid", color="black", weight=3];
28[label="addToFM_C2 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 (EQ == LT)",fontsize=16,color="black",shape="box"];28 -> 29[label="",style="solid", color="black", weight=3];
29[label="addToFM_C2 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 False",fontsize=16,color="black",shape="box"];29 -> 30[label="",style="solid", color="black", weight=3];
30[label="addToFM_C1 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 (() > ())",fontsize=16,color="black",shape="box"];30 -> 31[label="",style="solid", color="black", weight=3];
31[label="addToFM_C1 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 (compare () () == GT)",fontsize=16,color="black",shape="box"];31 -> 32[label="",style="solid", color="black", weight=3];
32[label="addToFM_C1 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 (EQ == GT)",fontsize=16,color="black",shape="box"];32 -> 33[label="",style="solid", color="black", weight=3];
33[label="addToFM_C1 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 False",fontsize=16,color="black",shape="box"];33 -> 34[label="",style="solid", color="black", weight=3];
34[label="addToFM_C0 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 otherwise",fontsize=16,color="black",shape="box"];34 -> 35[label="",style="solid", color="black", weight=3];
35[label="addToFM_C0 vyz3 () vyz41 vyz42 vyz43 vyz44 () vyz501 True",fontsize=16,color="black",shape="box"];35 -> 36[label="",style="solid", color="black", weight=3];
36[label="Branch () (vyz3 vyz41 vyz501) vyz42 vyz43 vyz44",fontsize=16,color="green",shape="box"];36 -> 37[label="",style="dashed", color="green", weight=3];
37[label="vyz3 vyz41 vyz501",fontsize=16,color="green",shape="box"];37 -> 38[label="",style="dashed", color="green", weight=3];
37 -> 39[label="",style="dashed", color="green", weight=3];
38[label="vyz41",fontsize=16,color="green",shape="box"];39[label="vyz501",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ QDP

                          ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldl(vyz3, :(vyz50, vyz51), h) → new_foldl(vyz3, vyz51, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldl(vyz3, :(vyz50, vyz51), h) → new_foldl(vyz3, vyz51, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

addToFM_C	combiner EmptyFM key elt	= addToFM_C4 combiner EmptyFM key elt
addToFM_C	combiner (Branch key elt size fm_l fm_r) new_key new_elt	= addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C2	combiner key elt size fm_l fm_r new_key new_elt True	= mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2	combiner key elt size fm_l fm_r new_key new_elt False	= addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

addToFM_C1	combiner key elt size fm_l fm_r new_key new_elt True	= mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1	combiner key elt size fm_l fm_r new_key new_elt False	= addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

addToFM_C4	combiner EmptyFM key elt	= unitFM key elt
addToFM_C4	vvx vvy vvz vwu	= addToFM_C3 vvx vvy vvz vwu

mkBalBranch11	fm_L fm_R yz zu zv fm_ll fm_lr True	= single_R fm_L fm_R
mkBalBranch11	fm_L fm_R yz zu zv fm_ll fm_lr False	= mkBalBranch10 fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch01	fm_L fm_R vuu vuv vuw fm_rl fm_rr True	= single_L fm_L fm_R
mkBalBranch01	fm_L fm_R vuu vuv vuw fm_rl fm_rr False	= mkBalBranch00 fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise

mkBranchLeft_ok0	vwx vwy vwz fm_l key EmptyFM	= True
mkBranchLeft_ok0	vwx vwy vwz fm_l key (Branch left_key wu wv ww wx)	= mkBranchLeft_ok0Biggest_left_key fm_l < key

mkBalBranch6MkBalBranch5	vxy vxz vyu vyv key elt fm_L fm_R True	= mkBranch 1 key elt fm_L fm_R
mkBalBranch6MkBalBranch5	vxy vxz vyu vyv key elt fm_L fm_R False	= mkBalBranch6MkBalBranch4 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_r vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_l vxy vxz vyu vyv)

mkBalBranch6MkBalBranch4	vxy vxz vyu vyv key elt fm_L fm_R True	= mkBalBranch6MkBalBranch0 vxy vxz vyu vyv fm_L fm_R fm_R
mkBalBranch6MkBalBranch4	vxy vxz vyu vyv key elt fm_L fm_R False	= mkBalBranch6MkBalBranch3 vxy vxz vyu vyv key elt fm_L fm_R (mkBalBranch6Size_l vxy vxz vyu vyv > sIZE_RATIO * mkBalBranch6Size_r vxy vxz vyu vyv)

mkBalBranch6MkBalBranch11	vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr True	= mkBalBranch6Single_R vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch11	vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr False	= mkBalBranch6MkBalBranch10 vxy vxz vyu vyv fm_L fm_R yz zu zv fm_ll fm_lr otherwise

mkBalBranch6MkBalBranch3	vxy vxz vyu vyv key elt fm_L fm_R True	= mkBalBranch6MkBalBranch1 vxy vxz vyu vyv fm_L fm_R fm_L
mkBalBranch6MkBalBranch3	vxy vxz vyu vyv key elt fm_L fm_R False	= mkBalBranch6MkBalBranch2 vxy vxz vyu vyv key elt fm_L fm_R otherwise

mkBalBranch6MkBalBranch01	vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr True	= mkBalBranch6Single_L vxy vxz vyu vyv fm_L fm_R
mkBalBranch6MkBalBranch01	vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr False	= mkBalBranch6MkBalBranch00 vxy vxz vyu vyv fm_L fm_R vuu vuv vuw fm_rl fm_rr otherwise